(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
g(c(x1)) → g(f(c(x1)))
g(f(c(x1))) → g(f(f(c(x1))))
g(g(x1)) → g(f(g(x1)))
f(f(g(x1))) → g(f(x1))
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
g(c(z0)) → g(f(c(z0)))
g(f(c(z0))) → g(f(f(c(z0))))
g(g(z0)) → g(f(g(z0)))
f(f(g(z0))) → g(f(z0))
Tuples:
G(c(z0)) → c1(G(f(c(z0))), F(c(z0)))
G(f(c(z0))) → c2(G(f(f(c(z0)))), F(f(c(z0))), F(c(z0)))
G(g(z0)) → c3(G(f(g(z0))), F(g(z0)), G(z0))
F(f(g(z0))) → c4(G(f(z0)), F(z0))
S tuples:
G(c(z0)) → c1(G(f(c(z0))), F(c(z0)))
G(f(c(z0))) → c2(G(f(f(c(z0)))), F(f(c(z0))), F(c(z0)))
G(g(z0)) → c3(G(f(g(z0))), F(g(z0)), G(z0))
F(f(g(z0))) → c4(G(f(z0)), F(z0))
K tuples:none
Defined Rule Symbols:
g, f
Defined Pair Symbols:
G, F
Compound Symbols:
c1, c2, c3, c4
(3) CdtUnreachableProof (EQUIVALENT transformation)
The following tuples could be removed as they are not reachable from basic start terms:
G(g(z0)) → c3(G(f(g(z0))), F(g(z0)), G(z0))
F(f(g(z0))) → c4(G(f(z0)), F(z0))
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
g(c(z0)) → g(f(c(z0)))
g(f(c(z0))) → g(f(f(c(z0))))
g(g(z0)) → g(f(g(z0)))
f(f(g(z0))) → g(f(z0))
Tuples:
G(c(z0)) → c1(G(f(c(z0))), F(c(z0)))
G(f(c(z0))) → c2(G(f(f(c(z0)))), F(f(c(z0))), F(c(z0)))
S tuples:
G(c(z0)) → c1(G(f(c(z0))), F(c(z0)))
G(f(c(z0))) → c2(G(f(f(c(z0)))), F(f(c(z0))), F(c(z0)))
K tuples:none
Defined Rule Symbols:
g, f
Defined Pair Symbols:
G
Compound Symbols:
c1, c2
(5) CdtGraphRemoveDanglingProof (ComplexityIfPolyImplication transformation)
Removed 2 of 2 dangling nodes:
G(c(z0)) → c1(G(f(c(z0))), F(c(z0)))
G(f(c(z0))) → c2(G(f(f(c(z0)))), F(f(c(z0))), F(c(z0)))
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
g(c(z0)) → g(f(c(z0)))
g(f(c(z0))) → g(f(f(c(z0))))
g(g(z0)) → g(f(g(z0)))
f(f(g(z0))) → g(f(z0))
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:
g, f
Defined Pair Symbols:none
Compound Symbols:none
(7) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(8) BOUNDS(O(1), O(1))